Nuprl Lemma : w-s_wf
11,40
postcript
pdf
the_w
:World,
i
:Id,
t
:
,
x
:Id. s(
i
;
t
).
x
vartype(
i
;
x
)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
vartype(
i
;
x
)
,
s(
i
;
t
).
x
,
w
.T
,
t
.1
,
t
.2
,
World
Lemmas
Id
wf
,
nat
wf
,
world
wf
origin
the_w:World, i:Id, t:
, x:Id. s(i;t).x 
vartype(i;x) the_w:World, i:Id, t:, x:Id. s(i;t).x vartype(i;x) x:A. B(x) T